…ation state (#83)

## Why

The Lean + Coq proof repair/extension landed in **#79–#82 (all merged)**
but was **invisible to the estate's bot-coordination layer**. The
machine-readable state still described a pre-proof-work world:

- `STATE.a2ml [frontier]` named only an aspirational Isabelle narrative
and **omitted the existing, now-verified Lean+Coq type-safety track**
entirely; `last-shepherd` stopped at #77.
- `debt.a2ml` carried **zero** real items — so the documented proof
follow-ups would not reach the next session's Phase 0.
- `coverage.a2ml` had no record that `docs/proofs/verification/` was
visited.
- `methodology.a2ml`'s divergent-mode invariants were generic template
stubs — one example literally read *"Idris2 only … no Lean4, Coq"*, the
**opposite** of reality, a real footgun for a divergent-mode bot.

## What (all additive; no curated content overwritten)

Surfaced through the channels whose own contracts say *"updated by
agents at session end"*:

| File | Change |
|---|---|
| `bot_directives/debt.a2ml` | Carry-forward follow-ups as Phase-0
input: **should** — Coq binop parity, Lean array typing (Coq's is a
ready template), `cap_subsumes_trans`; **could** — Coq `preservation`
clean rewrite, Lean float binops, echo-types L3 integration blueprint. |
| `bot_directives/coverage.a2ml` | `docs/proofs/verification/` recorded
as a visited component (PRs #79–#82). |
| `bot_directives/methodology.a2ml` | `divergent-invariants`: provers
are **Lean 4 + Coq** (not Idris2/Isabelle); admit/sorry stay **zero**;
the `Coq.Reals` axioms are **permitted, not escape hatches** (don't let
an Axiom-scanner flag them). `known-constraints`: CI-gated +
toolchain-pinned (Coq is version-sensitive); Lean/Coq cover
**complementary** subsets; PROOF-NEEDS #2 is **ill-posed** pending a
maintainer (a)/(b) decision. |
| `6a2/STATE.a2ml` | Added `type-safety-proofs` to `[frontier]`; added
`proof-gates` + `last-proof-shepherd` to `[ci]`. Existing lines
preserved. |

Source of truth for every claim:
[`docs/proofs/verification/AUDIT.md`](../blob/main/docs/proofs/verification/AUDIT.md).

## Notes for review

- **Draft on purpose** — `.machine_readable/` is maintainer-curated
(`gitbot-fleet`/`hypatia` are both barred from it), so this goes through
human review rather than direct-to-`main`.
- The only deletions are replaced **generic template-example comments**
in `methodology.a2ml` (incl. the misleading "Idris2 only" stub). No real
data removed.
- `coverage.a2ml`'s `total/visited` summary counters were left untouched
— I won't fabricate a component denominator.
- Stacked on the merged #82; the net diff is the four files above.

https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7

---
_Generated by [Claude
Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_

---------

Co-authored-by: Claude <noreply@anthropic.com>